(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun aa () Real)
(declare-fun d () Real)
(declare-fun g () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun s () Real)
(declare-fun t () Real)
(declare-fun o () Real)
(declare-fun ac () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(declare-fun af () Real)
(declare-fun ag () Real)
(declare-fun aj () Real)
(assert (not (exists ((o Real)) (=> (or (and (or (and (<= g ad) (< (+ j (/ (* (- aa af) (- aa af)) (* c j))) 0) (<= 0 a)) (<= 0 l)) (<= 0 (+ aa af)) (<= af l) (< 0 (/ 32 b (- e t)))) (<= 0 l) (< 0 ac)) (=> (<= 0 t) (not (=> (<= 0 o) (<= o ac))))))))
(assert (not (exists ((ak Real)) (=> (and (or (and (or (and (= (or (<= 0 p) (<= p (* g k))) (<= 0 (+ (* d i a) a))) (<= 0 (- a f)) (< 0 (- b m))) (< (+ h (/ (* (- a f) (- a f)) (* 2 q))) n)) (< n aj)) (<= ae m)) (< 0 (- m))) (<= 0 (+ (* (- d i) (- g k)) (- a f)))))))
(assert (= a (/ f r)))
(assert (= b (+ m ag)))
(assert (= c (+ n h)))
(assert (= g (+ k s ag)))
(assert (= e (+ t ag) (+ o p ac r)))
(check-sat)
